$\forall$$T$:Type. subtype\_rel($T$; $\mathbb{Z}$) $\Rightarrow$ ($\forall$${\it as}$,${\it bs}$:($T$ List). merge(${\it as}$; ${\it bs}$) $\in$ ($T$ List))